s{-}insert($x$;$l$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Case of $l$; nil $\rightarrow$ $x$.nil ; $a$.${\it as}$, rec:$v$ $\rightarrow$ if $x$=$_{2}$$a$$\rightarrow$ $a$.${\it as}$ ; $x$$<_{2}$$a$$\rightarrow$ [$x$; $a$/ ${\it as}$] else $a$.$v$ fi